\newcommand{\ObjectType}{ \typ{\Pi X. \AT{(\AT{Food}{X})}{\AT{(\AT{Obstacle}{X})}{\AT{(\AT{Pheromone}{X})}{X}}}}}
\noindent
To represent \SF{} terms and types, we use the implementation of the de Bruijn  canonical representation of variables and expressions \cite{Bru72} described in \cite{Pie02}. It has the advantage  of making $\alpha$-equivalence the same as syntactic equality. In this representation scheme, named variables are replaced by natural numbers, each  index is a number that represents an occurrence of a variable in an expression, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. Variable occurrences point directly to their binders, rather than being referenced by name. To use this representation scheme, the reading of an expression needs to be done in conjunction with a context.
\subsection{Contexts}
\input{context}
\input{debrujn}

%    \begin{definition}[Terminal Set]
%
%     Given $ty$ and $ty_p$, A set of terminals on $ty$, $F$ is composed of:
%       \begin{enumerate}
%       \item All elements of $ty$. These are called {\em atomic types} or {\em free type variables}.
%       \item All elements of $ty_p$.
%       \item Given a finite set of lower case symbol $te_p$, $(\alpha, \Gamma)$ is a terminal, where $\alpha\in te_p$ and $\Gamma$ is a type on $ty$ (but might be written using renaming rules in $ty_p$). For example, $(move, \typ{\AT{Direction}{Behavior}})$ or in the context of table \ref{tab:ctxex1}, $(gt, \typ{\AT{Int}{\AT{Int}{Boolean}}})$ with $\typ{Boolean}\in ty_p$.
%       \item Lower case names for \SF{} terms, possibly including free term variables and free type variables. The free term variables must be included in the terminal set as $(\alpha,\Gamma)$, with $\Gamma$ considered the type of the variable $\alpha$. Similarly, the free type variables are elements of $ty$. Within an expression, a type may also be represented as a name in $ty_p$.
%           For example, the symbol $true$ is included as a name for the term $(\Lambda X. \lambda x^{X}. \lambda y^X. x)$ in the context of table \ref{tab:tcs}.
%        \end{enumerate}
%     \end{definition}
